T:Type, eq:EqDecider(T), es:ES, x:Id, e:{e:E| @loc(e)(x:T)} . loc(lastchange(x;e)) ~ loc(e) 

latex

Definitions	s ~ t, SQType(T), {T}, <a, b>, {x:A| B(x)} , lastchange(x;e), left + right, Unit, x changed before e, if b then t else f fi , , , b, P  Q, P & Q, s = t, P  Q, P  Q, x:AB(x), A, False, @i(x:T), E, t.1, Id, Atom$n, ES, EqDecider(T), x:A  B(x), Type, isrcv(e), b, loc(e), x:A. B(x), t  T
Lemmas	es-loc wf, es-isrcv-loc, assert wf, not wf, bnot wf, bool wf, es-dtype wf, loc-last-change, changed wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, deq wf, event system wf, Id wf, es-E wf, Id sq